COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	| natural numbers								|
C00003 00003	declare INDCONST m0 n0 ε NATNUM
C00008 ENDMK
C⊗;
comment | natural numbers								|

DECLARE OPCONST +(NATNUM,NATNUM)=NATNUM[R←455,L←450];
DECLARE OPCONST -(NATNUM,NATNUM)=NATNUM[R←455,L←450];
DECLARE OPCONST *(NATNUM,NATNUM)=NATNUM[R←555,L←550];

DECLARE PREDCONST < ≤ > ≥(NATNUM,NATNUM) [INF];

ATTACH + ↔ (LAMBDA (X Y) (PLUS X Y));
ATTACH - ↔ (LAMBDA (X Y) (DIFFERENCE X Y));
ATTACH * ↔ (LAMBDA (X Y) (TIMES X Y));
ATTACH < ↔ (LAMBDA (X Y) (LESSP X Y));
ATTACH ≤ ↔ (LAMBDA (X Y) (OR (EQ X Y) (LESSP X Y)));
ATTACH < ↔ (LAMBDA (X Y) (LESSP Y X));
ATTACH ≥ ↔ (LAMBDA (X Y) (OR (EQ X Y) (LESSP Y X)));

declare INDCONST m0 n0 ε NATNUM;
declare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

declare INDCONST RW ε WORLD;
declare INDVAR w w1 w2 w3 ε WORLD;

declare OPCONST M(WORLD) = NATNUM;
declare OPCONST N(WORLD) = NATNUM;

declare INDCONST S P SP ε PERSON;
declare INDVAR s s0 s1 s2 ε PERSON;

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);
declare PREDCONST ok(NATNUM,NATNUM);

declare PREDCONST agree(WORLD,WORLD);

declare PREDPAR phi(WORLD,WORLD);

axiom agree:	∀w1 w2.(agree(w1,w2) ≡ M(w1) = M(w2) ∧ N(w1) = N(w2));;

axiom reflex:	∀w s m.A(w,w,s,m);;

axiom transitive:	∀w1 w2 w3 s m.(A(w1,w2,s,m) ∧ A(w2,w3,s,m) ⊃ A(w1,w3,s,m));;

axiom sp:	∀w1 w2 m.(A(w1,w2,S,m) ∨ A(w1,w2,P,m) ⊃ A(w1,w2,SP,m))

		∀m.(
		∀w1 w2.(A(w1,w2,S,m) ∨ A(w1,w2,P,m) ⊃ phi(w1,w2)) ∧
		∀w1 w2 w3.(phi(w1,w2) ∧ phi(w2,w3) ⊃ phi(w1,w3))
⊃	∀w1 w2.(phi(w1,w2) ⊃ A(w1,w2,SP,m)))
;;


axiom rw:	m0 = M(RW)
		n0 = N(RW)
;;

axiom ok:	∀m n.(ok(m,n) ≡ 1<m ∧ 1<n ∧ m≤n ∧ m<100 ∧ n<100)
		∀w.ok(M(w),N(w))
;;

axiom initial:
	∀w w1.(A(RW,w,SP,0) ∧ A(w,w1,S,0) ⊃ M(w1)+N(w1) = M(w)+N(w))
	∀w w1.(A(RW,w,SP,0) ∧ A(w,w1,P,0) ⊃ M(w1)*N(w1) = M(w)*N(w))
	∀w m n.(A(RW,w,SP,0) ∧ ok(m,n) ∧ M(w) + N(w) = m + n ⊃
∃w1.(A(w,w1,S,0) ∧ M(w1) = m ∧ N(w1) = n))
	∀w m n.(A(RW,w,SP,0) ∧ ok(m,n) ∧ M(w) * N(w) = m * n ⊃
∃w1.(A(w,w1,P,0) ∧ M(w1) = m ∧ N(w1) = n))
;;

axiom npk:
	∃w.(A(RW,w,P,0) ∧ ¬agree(RW,w))
;;

axiom sknpk:
	∀w.(A(RW,w,S,0) ⊃ ∃w1.(A(w,w1,P,0) ∧ ¬agree(w,w1)))
;;

axiom nsk:
	∃w.(A(RW,w,S,0) ∧ ¬agree(RW,w))
;;

axiom elsknpkansk:
	∀w.(A(RW,w,SP,1) ≡ A(RW,w,SP,0) ∧ 
∀w1.(A(w,w1,S,0) ⊃ ∃w2.(A(w1,w2,P,0) ∧ ¬agree(w1,w2))) ∧
∃w1.(A(w,w1,S,0) ∧ ¬agree(w,w1)))

	∀w1 w2.(A(w1,w2,S,1) ≡ A(w1,w2,S,0) ∧ A(w1,w2,SP,1))

	∀w1 w2.(A(w1,w2,P,1) ≡ A(w1,w2,P,0) ∧ A(w1,w2,SP,1))
;;

axiom pk:
	∀w.(A(RW,w,P,1) ⊃ agree(RW,w))
;;

axiom elpk:
	∀w.(A(RW,w,SP,2) ≡ A(RW,w,SP,1)
∧ ∀w1.(A(w,w1,P,1) ⊃ agree(w,w1)))

	∀w1 w2.(A(w1,w2,S,2) ≡ A(w1,w2,S,1) ∧ A(w1,w2,SP,2))

	∀w1 w2.(A(w1,w2,P,2) ≡ A(w1,w2,P,1) ∧ A(w1,w2,SP,2))
;;

axiom sk:	∀w.(A(RW,w,S,2) ⊃ agree(RW,w));;
	
MARK 1;

declare PREDCONST R0(NATNUM,NATNUM) R1(NATNUM,NATNUM) R2(NATNUM,NATNUM)
R3(NATNUM,NATNUM);

axiom R0:	∀m n.(R0(m,n) ≡ ok(m,n) ∧ ∃m1 n1.(ok(m1,n1) ∧ m1*n1 = m*n
∧ ¬(m1=m ∧ n1=n)))
;;

axiom R1:	∀m n.(R1(m,n) ≡ ok(m,n) ∧
			∀m1 n1.(ok(m1,n1) ∧ m1+n1 = m+n ⊃ R0(m1,n1)) ∧
			∃m1 n1.(m1+n1 = m+n ∧ ¬(m1=m ∧ n1=n)));;


axiom R2:	∀m n.(R2(m,n) ≡ ok(m,n) ∧ 
			∀m1 n1.(m1*n1 = m*n ∧ R1(m1,n1) ⊃ m1=m ∧ n1=n));;

axiom R3:	∀m n.(R3(m,n) ≡ ok(m,n) ∧
			∀m1 n1.(m1+n1 = m+n ∧ R2(m1,n1) ⊃ m1=m ∧ n1=n));;